$\forall$${\it es}$:ES, $e$:E, $l$:IdLnk, ${\it tg}$:Id.
\\[0ex]($e$ sends on $l$ with tag ${\it tg}$) $\Rightarrow$ (sender(es{-}first{-}from(${\it es}$;$e$;$l$;${\it tg}$)) = $e$)